\begin{tabbing} $\vdash$ \=$\forall$$A$:Type, $x$, $y$:$A$, $P$:($A$$\rightarrow\mathbb{P}$), $i$, $j$:$\mathbb{Z}$.\+ \\[0ex]($P$(if ($i$ =$_{0}$ $j$) then $x$ else $y$ fi )) $\Rightarrow$ ($P$(if ($i$ =$_{0}$ $j$) then $x$ else $y$ fi )) \- \end{tabbing}